M:MsgA, x:Id, v:(M.ds(x)). M.init(x,v)   

latex

Definitions	MsgA, M.ds(x), M.init(x,v), z != f(x)  P(a;z), suptype(S; T), , f(x)?z, left + right, Unit, P  Q, P & Q, x:A  B(x), x  dom(f), a:A fp B(a), f(x), x. t(x), P  Q, x.A(x), Type, Id, IdDeq, , s = t, , b, A, b, S  T, x:A. B(x), x:AB(x), Void, t  T, Top, f(a), #$n, , False
Lemmas	subtype rel self, int inc rationals, top wf, assert wf, not wf, bnot wf, bool wf, id-deq wf, Id wf, fpf-ap wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-cap wf, rationals wf, msga wf